Problem:
 0(1(2(3(4(x1))))) -> 0(2(3(1(4(x1)))))
 0(5(1(2(3(4(x1)))))) -> 0(1(2(5(3(4(x1))))))
 0(5(1(2(3(4(x1)))))) -> 0(5(2(1(3(4(x1))))))
 0(5(1(2(3(4(x1)))))) -> 5(0(2(3(1(4(x1))))))
 0(5(2(3(1(4(x1)))))) -> 0(1(5(2(3(4(x1))))))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6}
   transitions:
    01(11) -> 12*
    11(45) -> 46*
    11(43) -> 44*
    11(8) -> 9*
    51(55) -> 56*
    51(47) -> 48*
    51(41) -> 42*
    51(58) -> 59*
    21(10) -> 11*
    21(57) -> 58*
    21(42) -> 43*
    21(46) -> 47*
    31(40) -> 41*
    31(9) -> 10*
    41(7) -> 8*
    41(29) -> 30*
    41(31) -> 32*
    41(21) -> 22*
    41(23) -> 24*
    00(5) -> 6*
    00(2) -> 6*
    00(4) -> 6*
    00(1) -> 6*
    00(3) -> 6*
    10(5) -> 1*
    10(2) -> 1*
    10(4) -> 1*
    10(1) -> 1*
    10(3) -> 1*
    20(5) -> 2*
    20(2) -> 2*
    20(4) -> 2*
    20(1) -> 2*
    20(3) -> 2*
    30(5) -> 3*
    30(2) -> 3*
    30(4) -> 3*
    30(1) -> 3*
    30(3) -> 3*
    40(5) -> 4*
    40(2) -> 4*
    40(4) -> 4*
    40(1) -> 4*
    40(3) -> 4*
    50(5) -> 5*
    50(2) -> 5*
    50(4) -> 5*
    50(1) -> 5*
    50(3) -> 5*
    1 -> 29*
    2 -> 21*
    3 -> 31*
    4 -> 23*
    5 -> 7*
    8 -> 40*
    12 -> 55,6
    22 -> 8*
    24 -> 8*
    30 -> 8*
    32 -> 8*
    41 -> 57,45
    44 -> 11*
    48 -> 11*
    56 -> 6*
    59 -> 43*
  problem:
   
  Qed